WORST_CASE(?,O(n^3)) * Step 1: DependencyPairs WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),g(),Acons(x2,x1)) -> abfoldr#4(fa(),fb(x2),abfoldr#4(f(),g(),x1)) abfoldr#4(f(),g(),Bcons(x2,x1)) -> Bcons(x2,abfoldr#4(f(),g(),x1)) abfoldr#4(fa(),fb(x3),Bcons(x2,x1)) -> Bcons(plus#2(x2,x3),abfoldr#4(fa(),fb(x3),x1)) main(x1) -> abfoldr#4(f(),g(),x1) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1,g/0} - Obligation: innermost runtime complexity wrt. defined symbols {abfoldr#4,main,plus#2} and constructors {0,Acons,Bcons ,Nil,S,f,fa,fb,g} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs abfoldr#4#(x8,x4,Nil()) -> c_1() abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)) abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)) abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)) main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) plus#2#(x4,0()) -> c_6() plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: abfoldr#4#(x8,x4,Nil()) -> c_1() abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)) abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)) abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)) main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) plus#2#(x4,0()) -> c_6() plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak TRS: abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),g(),Acons(x2,x1)) -> abfoldr#4(fa(),fb(x2),abfoldr#4(f(),g(),x1)) abfoldr#4(f(),g(),Bcons(x2,x1)) -> Bcons(x2,abfoldr#4(f(),g(),x1)) abfoldr#4(fa(),fb(x3),Bcons(x2,x1)) -> Bcons(plus#2(x2,x3),abfoldr#4(fa(),fb(x3),x1)) main(x1) -> abfoldr#4(f(),g(),x1) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/0,c_2/2,c_3/1,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {abfoldr#4#,main#,plus#2#} and constructors {0,Acons,Bcons ,Nil,S,f,fa,fb,g} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,6} by application of Pre({1,6}) = {2,3,4,5,7}. Here rules are labelled as follows: 1: abfoldr#4#(x8,x4,Nil()) -> c_1() 2: abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)) 3: abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)) 4: abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)) 5: main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) 6: plus#2#(x4,0()) -> c_6() 7: plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)) abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)) abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)) main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak DPs: abfoldr#4#(x8,x4,Nil()) -> c_1() plus#2#(x4,0()) -> c_6() - Weak TRS: abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),g(),Acons(x2,x1)) -> abfoldr#4(fa(),fb(x2),abfoldr#4(f(),g(),x1)) abfoldr#4(f(),g(),Bcons(x2,x1)) -> Bcons(x2,abfoldr#4(f(),g(),x1)) abfoldr#4(fa(),fb(x3),Bcons(x2,x1)) -> Bcons(plus#2(x2,x3),abfoldr#4(fa(),fb(x3),x1)) main(x1) -> abfoldr#4(f(),g(),x1) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/0,c_2/2,c_3/1,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {abfoldr#4#,main#,plus#2#} and constructors {0,Acons,Bcons ,Nil,S,f,fa,fb,g} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)) -->_1 abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)):3 -->_2 abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)):2 -->_2 abfoldr#4#(x8,x4,Nil()) -> c_1():6 -->_1 abfoldr#4#(x8,x4,Nil()) -> c_1():6 -->_2 abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)):1 2:S:abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)) -->_1 abfoldr#4#(x8,x4,Nil()) -> c_1():6 -->_1 abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)):2 -->_1 abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)):1 3:S:abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)) -->_1 plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)):5 -->_1 plus#2#(x4,0()) -> c_6():7 -->_2 abfoldr#4#(x8,x4,Nil()) -> c_1():6 -->_2 abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)):3 4:S:main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) -->_1 abfoldr#4#(x8,x4,Nil()) -> c_1():6 -->_1 abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)):2 -->_1 abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)):1 5:S:plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) -->_1 plus#2#(x4,0()) -> c_6():7 -->_1 plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)):5 6:W:abfoldr#4#(x8,x4,Nil()) -> c_1() 7:W:plus#2#(x4,0()) -> c_6() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 6: abfoldr#4#(x8,x4,Nil()) -> c_1() 7: plus#2#(x4,0()) -> c_6() * Step 4: RemoveHeads WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)) abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)) abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)) main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak TRS: abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),g(),Acons(x2,x1)) -> abfoldr#4(fa(),fb(x2),abfoldr#4(f(),g(),x1)) abfoldr#4(f(),g(),Bcons(x2,x1)) -> Bcons(x2,abfoldr#4(f(),g(),x1)) abfoldr#4(fa(),fb(x3),Bcons(x2,x1)) -> Bcons(plus#2(x2,x3),abfoldr#4(fa(),fb(x3),x1)) main(x1) -> abfoldr#4(f(),g(),x1) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/0,c_2/2,c_3/1,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {abfoldr#4#,main#,plus#2#} and constructors {0,Acons,Bcons ,Nil,S,f,fa,fb,g} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)) -->_1 abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)):3 -->_2 abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)):2 -->_2 abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)):1 2:S:abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)) -->_1 abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)):2 -->_1 abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)):1 3:S:abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)) -->_1 plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)):5 -->_2 abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)):3 4:S:main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) -->_1 abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)):2 -->_1 abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)):1 5:S:plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) -->_1 plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)):5 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(4,main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)))] * Step 5: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)) abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)) abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)) plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak TRS: abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),g(),Acons(x2,x1)) -> abfoldr#4(fa(),fb(x2),abfoldr#4(f(),g(),x1)) abfoldr#4(f(),g(),Bcons(x2,x1)) -> Bcons(x2,abfoldr#4(f(),g(),x1)) abfoldr#4(fa(),fb(x3),Bcons(x2,x1)) -> Bcons(plus#2(x2,x3),abfoldr#4(fa(),fb(x3),x1)) main(x1) -> abfoldr#4(f(),g(),x1) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/0,c_2/2,c_3/1,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {abfoldr#4#,main#,plus#2#} and constructors {0,Acons,Bcons ,Nil,S,f,fa,fb,g} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),g(),Acons(x2,x1)) -> abfoldr#4(fa(),fb(x2),abfoldr#4(f(),g(),x1)) abfoldr#4(f(),g(),Bcons(x2,x1)) -> Bcons(x2,abfoldr#4(f(),g(),x1)) abfoldr#4(fa(),fb(x3),Bcons(x2,x1)) -> Bcons(plus#2(x2,x3),abfoldr#4(fa(),fb(x3),x1)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)) abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)) abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)) plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) * Step 6: DecomposeDG WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)) abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)) abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)) plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak TRS: abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),g(),Acons(x2,x1)) -> abfoldr#4(fa(),fb(x2),abfoldr#4(f(),g(),x1)) abfoldr#4(f(),g(),Bcons(x2,x1)) -> Bcons(x2,abfoldr#4(f(),g(),x1)) abfoldr#4(fa(),fb(x3),Bcons(x2,x1)) -> Bcons(plus#2(x2,x3),abfoldr#4(fa(),fb(x3),x1)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/0,c_2/2,c_3/1,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {abfoldr#4#,main#,plus#2#} and constructors {0,Acons,Bcons ,Nil,S,f,fa,fb,g} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)) abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)) and a lower component abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)) plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) Further, following extension rules are added to the lower component. abfoldr#4#(f(),g(),Acons(x2,x1)) -> abfoldr#4#(f(),g(),x1) abfoldr#4#(f(),g(),Acons(x2,x1)) -> abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) abfoldr#4#(f(),g(),Bcons(x2,x1)) -> abfoldr#4#(f(),g(),x1) ** Step 6.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)) abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)) - Weak TRS: abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),g(),Acons(x2,x1)) -> abfoldr#4(fa(),fb(x2),abfoldr#4(f(),g(),x1)) abfoldr#4(f(),g(),Bcons(x2,x1)) -> Bcons(x2,abfoldr#4(f(),g(),x1)) abfoldr#4(fa(),fb(x3),Bcons(x2,x1)) -> Bcons(plus#2(x2,x3),abfoldr#4(fa(),fb(x3),x1)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/0,c_2/2,c_3/1,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {abfoldr#4#,main#,plus#2#} and constructors {0,Acons,Bcons ,Nil,S,f,fa,fb,g} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)) -->_2 abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)):2 -->_2 abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)):1 2:S:abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)) -->_1 abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)):2 -->_1 abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) ,abfoldr#4#(f(),g(),x1)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(f(),g(),x1)) ** Step 6.a:2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(f(),g(),x1)) abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)) - Weak TRS: abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),g(),Acons(x2,x1)) -> abfoldr#4(fa(),fb(x2),abfoldr#4(f(),g(),x1)) abfoldr#4(f(),g(),Bcons(x2,x1)) -> Bcons(x2,abfoldr#4(f(),g(),x1)) abfoldr#4(fa(),fb(x3),Bcons(x2,x1)) -> Bcons(plus#2(x2,x3),abfoldr#4(fa(),fb(x3),x1)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/0,c_2/1,c_3/1,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {abfoldr#4#,main#,plus#2#} and constructors {0,Acons,Bcons ,Nil,S,f,fa,fb,g} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(f(),g(),x1)) abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)) ** Step 6.a:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(f(),g(),x1)) abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/0,c_2/1,c_3/1,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {abfoldr#4#,main#,plus#2#} and constructors {0,Acons,Bcons ,Nil,S,f,fa,fb,g} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- Acons :: ["A"(0) x "A"(15)] -(15)-> "A"(15) Bcons :: ["A"(15) x "A"(15)] -(15)-> "A"(15) f :: [] -(0)-> "A"(0) f :: [] -(0)-> "A"(14) g :: [] -(0)-> "A"(0) g :: [] -(0)-> "A"(4) g :: [] -(0)-> "A"(12) abfoldr#4# :: ["A"(0) x "A"(0) x "A"(15)] -(0)-> "A"(0) c_2 :: ["A"(0)] -(0)-> "A"(0) c_3 :: ["A"(0)] -(0)-> "A"(14) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "Acons_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "Bcons_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "c_2_A" :: ["A"(0)] -(0)-> "A"(1) "c_3_A" :: ["A"(0)] -(0)-> "A"(1) "f_A" :: [] -(0)-> "A"(1) "g_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)) 2. Weak: abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(f(),g(),x1)) ** Step 6.a:4: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(f(),g(),x1)) - Weak DPs: abfoldr#4#(f(),g(),Bcons(x2,x1)) -> c_3(abfoldr#4#(f(),g(),x1)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/0,c_2/1,c_3/1,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {abfoldr#4#,main#,plus#2#} and constructors {0,Acons,Bcons ,Nil,S,f,fa,fb,g} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- Acons :: ["A"(0) x "A"(15)] -(15)-> "A"(15) Bcons :: ["A"(0) x "A"(15)] -(15)-> "A"(15) f :: [] -(0)-> "A"(0) f :: [] -(0)-> "A"(10) g :: [] -(0)-> "A"(0) g :: [] -(0)-> "A"(14) abfoldr#4# :: ["A"(0) x "A"(0) x "A"(15)] -(7)-> "A"(0) c_2 :: ["A"(0)] -(0)-> "A"(0) c_3 :: ["A"(0)] -(0)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "Acons_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "Bcons_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "c_2_A" :: ["A"(0)] -(0)-> "A"(1) "c_3_A" :: ["A"(0)] -(0)-> "A"(1) "f_A" :: [] -(0)-> "A"(1) "g_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: abfoldr#4#(f(),g(),Acons(x2,x1)) -> c_2(abfoldr#4#(f(),g(),x1)) 2. Weak: ** Step 6.b:1: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)) plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak DPs: abfoldr#4#(f(),g(),Acons(x2,x1)) -> abfoldr#4#(f(),g(),x1) abfoldr#4#(f(),g(),Acons(x2,x1)) -> abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) abfoldr#4#(f(),g(),Bcons(x2,x1)) -> abfoldr#4#(f(),g(),x1) - Weak TRS: abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),g(),Acons(x2,x1)) -> abfoldr#4(fa(),fb(x2),abfoldr#4(f(),g(),x1)) abfoldr#4(f(),g(),Bcons(x2,x1)) -> Bcons(x2,abfoldr#4(f(),g(),x1)) abfoldr#4(fa(),fb(x3),Bcons(x2,x1)) -> Bcons(plus#2(x2,x3),abfoldr#4(fa(),fb(x3),x1)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/0,c_2/2,c_3/1,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {abfoldr#4#,main#,plus#2#} and constructors {0,Acons,Bcons ,Nil,S,f,fa,fb,g} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component abfoldr#4#(f(),g(),Acons(x2,x1)) -> abfoldr#4#(f(),g(),x1) abfoldr#4#(f(),g(),Acons(x2,x1)) -> abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) abfoldr#4#(f(),g(),Bcons(x2,x1)) -> abfoldr#4#(f(),g(),x1) abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)) and a lower component plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) Further, following extension rules are added to the lower component. abfoldr#4#(f(),g(),Acons(x2,x1)) -> abfoldr#4#(f(),g(),x1) abfoldr#4#(f(),g(),Acons(x2,x1)) -> abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) abfoldr#4#(f(),g(),Bcons(x2,x1)) -> abfoldr#4#(f(),g(),x1) abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> abfoldr#4#(fa(),fb(x3),x1) abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> plus#2#(x2,x3) *** Step 6.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)) - Weak DPs: abfoldr#4#(f(),g(),Acons(x2,x1)) -> abfoldr#4#(f(),g(),x1) abfoldr#4#(f(),g(),Acons(x2,x1)) -> abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) abfoldr#4#(f(),g(),Bcons(x2,x1)) -> abfoldr#4#(f(),g(),x1) - Weak TRS: abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),g(),Acons(x2,x1)) -> abfoldr#4(fa(),fb(x2),abfoldr#4(f(),g(),x1)) abfoldr#4(f(),g(),Bcons(x2,x1)) -> Bcons(x2,abfoldr#4(f(),g(),x1)) abfoldr#4(fa(),fb(x3),Bcons(x2,x1)) -> Bcons(plus#2(x2,x3),abfoldr#4(fa(),fb(x3),x1)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/0,c_2/2,c_3/1,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {abfoldr#4#,main#,plus#2#} and constructors {0,Acons,Bcons ,Nil,S,f,fa,fb,g} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)) -->_2 abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)):1 2:W:abfoldr#4#(f(),g(),Acons(x2,x1)) -> abfoldr#4#(f(),g(),x1) -->_1 abfoldr#4#(f(),g(),Bcons(x2,x1)) -> abfoldr#4#(f(),g(),x1):4 -->_1 abfoldr#4#(f(),g(),Acons(x2,x1)) -> abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)):3 -->_1 abfoldr#4#(f(),g(),Acons(x2,x1)) -> abfoldr#4#(f(),g(),x1):2 3:W:abfoldr#4#(f(),g(),Acons(x2,x1)) -> abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) -->_1 abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(plus#2#(x2,x3),abfoldr#4#(fa(),fb(x3),x1)):1 4:W:abfoldr#4#(f(),g(),Bcons(x2,x1)) -> abfoldr#4#(f(),g(),x1) -->_1 abfoldr#4#(f(),g(),Bcons(x2,x1)) -> abfoldr#4#(f(),g(),x1):4 -->_1 abfoldr#4#(f(),g(),Acons(x2,x1)) -> abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)):3 -->_1 abfoldr#4#(f(),g(),Acons(x2,x1)) -> abfoldr#4#(f(),g(),x1):2 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(abfoldr#4#(fa(),fb(x3),x1)) *** Step 6.b:1.a:2: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(abfoldr#4#(fa(),fb(x3),x1)) - Weak DPs: abfoldr#4#(f(),g(),Acons(x2,x1)) -> abfoldr#4#(f(),g(),x1) abfoldr#4#(f(),g(),Acons(x2,x1)) -> abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) abfoldr#4#(f(),g(),Bcons(x2,x1)) -> abfoldr#4#(f(),g(),x1) - Weak TRS: abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),g(),Acons(x2,x1)) -> abfoldr#4(fa(),fb(x2),abfoldr#4(f(),g(),x1)) abfoldr#4(f(),g(),Bcons(x2,x1)) -> Bcons(x2,abfoldr#4(f(),g(),x1)) abfoldr#4(fa(),fb(x3),Bcons(x2,x1)) -> Bcons(plus#2(x2,x3),abfoldr#4(fa(),fb(x3),x1)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/0,c_2/2,c_3/1,c_4/1,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {abfoldr#4#,main#,plus#2#} and constructors {0,Acons,Bcons ,Nil,S,f,fa,fb,g} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> "A"(0) Acons :: ["A"(0) x "A"(1)] -(0)-> "A"(1) Bcons :: ["A"(0) x "A"(1)] -(1)-> "A"(1) Nil :: [] -(0)-> "A"(1) Nil :: [] -(0)-> "A"(7) S :: ["A"(0)] -(0)-> "A"(0) S :: ["A"(0)] -(0)-> "A"(14) abfoldr#4 :: ["A"(1) x "A"(0) x "A"(1)] -(0)-> "A"(1) f :: [] -(0)-> "A"(1) f :: [] -(0)-> "A"(15) fa :: [] -(0)-> "A"(1) fa :: [] -(0)-> "A"(15) fb :: ["A"(0)] -(0)-> "A"(1) fb :: ["A"(0)] -(0)-> "A"(0) fb :: ["A"(0)] -(0)-> "A"(8) fb :: ["A"(0)] -(0)-> "A"(4) fb :: ["A"(0)] -(0)-> "A"(14) g :: [] -(0)-> "A"(0) g :: [] -(0)-> "A"(1) g :: [] -(0)-> "A"(7) plus#2 :: ["A"(0) x "A"(0)] -(0)-> "A"(0) abfoldr#4# :: ["A"(1) x "A"(1) x "A"(1)] -(5)-> "A"(8) c_4 :: ["A"(0)] -(0)-> "A"(8) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "0_A" :: [] -(0)-> "A"(1) "Acons_A" :: ["A"(0) x "A"(1)] -(0)-> "A"(1) "Bcons_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "Nil_A" :: [] -(0)-> "A"(1) "S_A" :: ["A"(0)] -(0)-> "A"(1) "c_4_A" :: ["A"(0)] -(0)-> "A"(1) "f_A" :: [] -(0)-> "A"(1) "fa_A" :: [] -(0)-> "A"(1) "fb_A" :: ["A"(0)] -(0)-> "A"(1) "g_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> c_4(abfoldr#4#(fa(),fb(x3),x1)) 2. Weak: *** Step 6.b:1.b:1: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak DPs: abfoldr#4#(f(),g(),Acons(x2,x1)) -> abfoldr#4#(f(),g(),x1) abfoldr#4#(f(),g(),Acons(x2,x1)) -> abfoldr#4#(fa(),fb(x2),abfoldr#4(f(),g(),x1)) abfoldr#4#(f(),g(),Bcons(x2,x1)) -> abfoldr#4#(f(),g(),x1) abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> abfoldr#4#(fa(),fb(x3),x1) abfoldr#4#(fa(),fb(x3),Bcons(x2,x1)) -> plus#2#(x2,x3) - Weak TRS: abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),g(),Acons(x2,x1)) -> abfoldr#4(fa(),fb(x2),abfoldr#4(f(),g(),x1)) abfoldr#4(f(),g(),Bcons(x2,x1)) -> Bcons(x2,abfoldr#4(f(),g(),x1)) abfoldr#4(fa(),fb(x3),Bcons(x2,x1)) -> Bcons(plus#2(x2,x3),abfoldr#4(fa(),fb(x3),x1)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/0,c_2/2,c_3/1,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {abfoldr#4#,main#,plus#2#} and constructors {0,Acons,Bcons ,Nil,S,f,fa,fb,g} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> "A"(0) Acons :: ["A"(13) x "A"(13)] -(13)-> "A"(13) Acons :: ["A"(14) x "A"(14)] -(14)-> "A"(14) Bcons :: ["A"(0) x "A"(13)] -(0)-> "A"(13) Bcons :: ["A"(0) x "A"(14)] -(0)-> "A"(14) Nil :: [] -(0)-> "A"(13) Nil :: [] -(0)-> "A"(15) S :: ["A"(1)] -(1)-> "A"(1) S :: ["A"(0)] -(0)-> "A"(0) abfoldr#4 :: ["A"(1) x "A"(0) x "A"(13)] -(8)-> "A"(14) f :: [] -(0)-> "A"(1) f :: [] -(0)-> "A"(15) fa :: [] -(0)-> "A"(1) fa :: [] -(0)-> "A"(15) fb :: ["A"(0)] -(0)-> "A"(0) fb :: ["A"(1)] -(1)-> "A"(1) g :: [] -(0)-> "A"(0) g :: [] -(0)-> "A"(1) g :: [] -(0)-> "A"(7) plus#2 :: ["A"(0) x "A"(0)] -(0)-> "A"(0) abfoldr#4# :: ["A"(1) x "A"(1) x "A"(14)] -(8)-> "A"(1) plus#2# :: ["A"(0) x "A"(1)] -(1)-> "A"(1) c_7 :: ["A"(0)] -(0)-> "A"(12) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "0_A" :: [] -(0)-> "A"(1) "Acons_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "Bcons_A" :: ["A"(0) x "A"(1)] -(0)-> "A"(1) "Nil_A" :: [] -(0)-> "A"(1) "S_A" :: ["A"(1)] -(1)-> "A"(1) "c_7_A" :: ["A"(0)] -(0)-> "A"(1) "f_A" :: [] -(0)-> "A"(1) "fa_A" :: [] -(0)-> "A"(1) "fb_A" :: ["A"(1)] -(1)-> "A"(1) "g_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) 2. Weak: WORST_CASE(?,O(n^3))